ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a:ecl(ds; da), v:ecl-trans-tuple{i:l}(ds; da),
L:(event-info(ds;da) List).
(L:(event-info(ds;da) List). 
(ecl-trans-normal(v)  (n:. (ecl-trans-halt2(ds; da; v)(n,L))  (n  ecl-trans-es(v))))
 (n:. 
 (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (ecl-halt(ds; da; a)(n,L'))))
  (ecl-trans-halt2(ds; da; v)(n,L)))
 (m:. (ecl-act(ds; da; m; a)(L))  (ecl-trans-act(ds; da; v)(m,L))))
 (n:. 
 (L':event-info(ds;da) List
 ((iseg(event-info(ds;da); L'; L)
 ( (0 < n)
 ( (star-append(event-info(ds;da); (ecl-halt(ds; da; a)(0)); (ecl-halt(ds; da; a)(n)))(L'))))
  (ecl-trans-halt2(ds; da; reset-ecl-tuple(v))(n,L))) 

latex

Definitions

P  Q, t.1, ecl-trans-type(A), ecl-trans-tuple{i:l}(ds; da), Y, ||as||, tt, ff, if b then t else f fi , spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-h(v), reset-ecl-tuple(A), True, T, ecl-trans-halt2(ds; da; A), A c B, P  Q, x:A. B(x), P  Q, P  Q, , ge(i; j), False, A, A  B, prop{i:l}, x. t(x), subtype(S; T), top, t  T, guard(T), P  Q, x:A. B(x), b, decidable(P), iseg(T; l1; l2), Unit, , x(s), ecl-trans-state(v; L),

Lemmas

bfalse wf, append iseg, length-append, subtype rel self, ma-valtype wf, decl-state wf, decidable assert, decidable functionality, ecl-reset-init, ecl-trans-state-from wf, ecl-trans-state-append, append assoc, iseg append0, member wf, non neg length, ecl-halt-nil, add functionality wrt eq, length append, append wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert of eq int, eqtt to assert, iff transitivity, eq int wf, ecl-trans-type wf, common iseg compat, ecl-halt-unique, ecl-reset-state, ecl-trans-state wf, ecl-trans-h wf, bool wf, true wf, squash wf, assert wf, iseg transitivity, iseg weakening, star-append-iff, ecl-trans-act wf, ecl-act wf, iff wf, ecl-trans-es wf, l member wf, nat plus inc, nat plus wf, ecl-trans-normal wf, reset-ecl-tuple wf, ecl-trans-halt2 wf, ecl-halt wf, star-append wf, iseg wf, ge wf, nat properties, le wf, Id wf, Knd wf, fpf wf, ecl wf, ecl-trans-tuple wf, event-info wf, length wf1, top wf, length wf nat, nat wf